/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BAXB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRK30
␈↓ ↓H␈↓␈↓ εH␈↓ 91


␈↓ ↓H␈↓α␈↓ επChapter I

␈↓ ↓H␈↓α␈↓ ∧(PROVING LISP PROGRAMS CORRECT


␈↓ ↓H␈↓␈↓ α_The␈αtheory␈αof␈αcomputation␈α
may␈αbe␈αdivided␈αinto␈αtwo␈α
parts.␈α The␈αfirst␈αis␈αthe␈α
general␈αtheory
␈↓ ↓H␈↓of␈α
computability␈α
including␈α
topics␈α
like␈α
universal␈α
functions,␈α
the␈α
existence␈α
of␈αuncomputable␈α
functions,
␈↓ ↓H␈↓lambda␈α
calculus,␈α
call-by-name␈α
and␈α
call-by-value,␈α
and␈α
the␈α
relation␈α
of␈α
conditional␈α
form␈α
recursion␈α
to
␈↓ ↓H␈↓other␈αformalisms␈αfor␈αdescribing␈αcomputable␈αfunctions.␈α The␈αsecond␈αpart,␈αwhich␈αwe␈αwill␈αdiscuss␈αin
␈↓ ↓H␈↓this␈α∪chapter␈α∪emphasizes␈α∩techniques␈α∪for␈α∪proving␈α∩particular␈α∪facts␈α∪about␈α∪particular␈α∩computable
␈↓ ↓H␈↓functions.  We emphasize the use of the techniques more than their mathematical background.

␈↓ ↓H␈↓␈↓ α_We␈αshall␈αconfine␈αourselves␈αto␈αproving␈α␈↓↓extensional␈αproperties␈↓␈αof␈α␈↓↓clean,␈αpure␈↓␈αLISP␈α
programs.
␈↓ ↓H␈↓An␈α⊂␈↓↓extensional␈α⊂property␈↓␈α⊂is␈α⊃one␈α⊂that␈α⊂depends␈α⊂only␈α⊂on␈α⊃the␈α⊂function␈α⊂computed␈α⊂by␈α⊃the␈α⊂program.
␈↓ ↓H␈↓Thus␈α∞it␈α∞includes␈α∞the␈α∞fact␈α∂that␈α∞two␈α∞sort␈α∞programs␈α∞compute␈α∂the␈α∞same␈α∞function␈α∞or␈α∞that␈α∂␈↓↓append␈↓␈α∞is
␈↓ ↓H␈↓associative␈αbut␈αdoes␈αnot␈αinclude␈αthe␈αfact␈αthat␈αone␈αsort␈αprogram␈αdoes␈α␈↓↓n␈↓∧2␈↓␈αcomparisons␈αand␈αanother
␈↓ ↓H␈↓␈↓↓n log n␈↓␈α
comparisons.␈α
 ␈↓↓Clean␈↓␈α
LISP␈α
programs␈α
have␈α
no␈α
side␈α
effects␈α
(our␈α
methods␈α
require␈αthe␈α
freedom
␈↓ ↓H␈↓to␈α
replace␈αa␈α
subexpression␈αby␈α
an␈αequal␈α
expression),␈αand␈α
equality␈αrefers␈α
to␈αthe␈α
S-expressions␈αand
␈↓ ↓H␈↓not␈αto␈αthe␈αlist␈αstructures.␈α ␈↓↓Pure␈↓␈αLISP␈αinvolves␈αonly␈αrecursive␈αfunction␈αdefinitions␈αand␈α
doesn't␈αuse
␈↓ ↓H␈↓assignment␈αstatements.␈α
 It␈αwouldn't␈α
be␈αdifficult␈α
to␈αgive␈α
corresponding␈αmethods␈α
that␈αwould␈αbe␈α
valid
␈↓ ↓H␈↓for non-functional programs, because this topic is well developed.

␈↓ ↓H␈↓␈↓ α_In␈α⊂spite␈α⊂of␈α∂all␈α⊂these␈α⊂limitations,␈α⊂the␈α∂techniques␈α⊂are␈α⊂useful␈α⊂and␈α∂point␈α⊂the␈α⊂way␈α⊂to␈α∂further
␈↓ ↓H␈↓progress.

␈↓ ↓H␈↓␈↓ α_The␈α necessary␈αbasic␈αfacts␈αcan␈αbe␈αdivided␈αinto␈αseveral␈αcategories:␈αfirst␈αorder␈αlogic␈αincluding
␈↓ ↓H␈↓conditional␈α↔forms␈α_and␈α↔first␈α↔order␈α_lambda-expressions,␈α↔algebraic␈α↔facts␈α_about␈α↔lists␈α_and␈α↔S-
␈↓ ↓H␈↓expressions,␈αfacts␈αabout␈αthe␈αinductive␈αstructure␈αof␈αlists␈αand␈αS-expressions,␈αand␈αgeneral␈αfacts␈αabout
␈↓ ↓H␈↓functions defined by recursion.



␈↓ ↓H␈↓1.  ␈↓αFirst order logic with conditional forms and lambda-expressions.␈↓


␈↓ ↓H␈↓␈↓ α_The␈α∂logic␈α∂we␈α∂shall␈α∂use␈α∂is␈α∂called␈α∂first␈α∂order␈α∂logic␈α∂with␈α∂equality,␈α∂but␈α∂we␈α∂will␈α∂extend␈α⊂it␈α∂by
␈↓ ↓H␈↓admitting␈α⊂conditional␈α⊃forms␈α⊂as␈α⊂terms␈α⊃and␈α⊂first␈α⊂order␈α⊃lambda-expressions␈α⊂as␈α⊃function␈α⊂symbols.
␈↓ ↓H␈↓These␈αextensions␈αdo␈αnot␈αchange␈αthe␈αlogical␈αstrength␈αof␈αthe␈αtheory,␈αbecause,␈αas␈αwe␈αshall␈αsee,␈αevery
␈↓ ↓H␈↓sentence␈α∩that␈α∩includes␈α∩conditional␈α∪forms␈α∩or␈α∩first␈α∩order␈α∪lambdas␈α∩can␈α∩be␈α∩transformed␈α∪into␈α∩an
␈↓ ↓H␈↓equivalent␈α
sentence␈α
without␈α
them.␈α
 However,␈αthe␈α
extensions␈α
are␈α
practically␈α
important,␈αbecause␈α
they
␈↓ ↓H␈↓permit us to use recursive definitions directly as formulas of the logic.

␈↓ ↓H␈↓␈↓ α_Formulas␈α∂of␈α∞the␈α∂logic␈α∞are␈α∂built␈α∂from␈α∞constants,␈α∂variables␈α∞predicate␈α∂symbols,␈α∂and␈α∞function
␈↓ ↓H␈↓symbols␈α⊂using␈α⊂function␈α∂application,␈α⊂conditional␈α⊂forms,␈α∂boolean␈α⊂forms,␈α⊂lambda␈α⊂expressions,␈α∂and
␈↓ ↓H␈↓quantifiers.

␈↓ ↓H␈↓␈↓αConstants␈↓:␈α∞We␈α
will␈α∞use␈α∞S-expresssions␈α
as␈α∞constants␈α
standing␈α∞for␈α∞themselves␈α
and␈α∞also␈α∞lower␈α
case
␈↓ ↓H␈↓letters␈α∩from␈α∩the␈α∩first␈α∩part␈α∩of␈α∩the␈α∪alphabet␈α∩to␈α∩represent␈α∩constants␈α∩in␈α∩other␈α∩domains␈α∪than␈α∩S-
␈↓ ↓H␈↓expressions.
␈↓ ↓H␈↓␈↓ ¬oCHAPTER I␈↓ 92


␈↓ ↓H␈↓␈↓αVariables␈↓:␈αWe␈αwill␈αuse␈αthe␈αletters␈α␈↓↓u␈↓␈αthru␈α␈↓↓z␈↓␈αwith␈αor␈αwithout␈αsubscripts␈αas␈αvariables.␈α The␈αvariables
␈↓ ↓H␈↓␈↓↓u␈↓␈α∂and␈α∞␈↓↓v␈↓␈α∂will␈α∞usually␈α∂stand␈α∞for␈α∂lists,␈α∞while␈α∂␈↓↓x␈↓␈α∞thru␈α∂␈↓↓z␈↓␈α∞will␈α∂stand␈α∞for␈α∂S-expressions.␈α∞ ␈↓↓m␈↓␈α∂and␈α∂␈↓↓n␈↓␈α∞are
␈↓ ↓H␈↓integer variables.

␈↓ ↓H␈↓␈↓αFunction␈αsymbols␈↓:␈αThe␈α
letters␈α␈↓↓f␈↓,␈α␈↓↓g␈↓␈α
and␈α␈↓↓h␈↓␈αwith␈α
or␈αwithout␈αsubscripts␈α
are␈αused␈αas␈αfunction␈α
symbols.
␈↓ ↓H␈↓The␈α⊂LISP␈α⊃function␈α⊂symbols␈α⊃␈↓αa␈↓,␈α⊂␈↓αd␈↓␈α⊃and␈α⊂.␈α⊃(as␈α⊂an␈α⊃infix)␈α⊂are␈α⊃also␈α⊂used␈α⊃as␈α⊂function␈α⊃symbols.␈α⊂ We
␈↓ ↓H␈↓suppose␈α
that␈αeach␈α
function␈αsymbol␈α
takes␈αthe␈α
same␈αdefinite␈α
number␈αof␈α
arguments␈αevery␈α
time␈α
it␈αis
␈↓ ↓H␈↓used.␈α Thus␈αif␈αthe␈αsame␈αletter␈αis␈αused␈αwith␈αdiffering␈αnumbers␈αof␈αarguments,␈αit␈αstands␈αfor␈αdifferent
␈↓ ↓H␈↓function␈αsymbols.␈α Thus␈αwe␈αcan␈αuse␈α␈↓↓<x␈↓β1␈↓↓,␈α...␈α,x␈↓βn␈↓↓>␈↓␈αto␈αrepresent␈αthe␈αlist␈αforming␈αfunctions,␈αbut␈αwe
␈↓ ↓H␈↓shall␈α∂have␈α∂to␈α∂axiomatize␈α∂it␈α⊂separately␈α∂for␈α∂each␈α∂length␈α∂we␈α⊂actually␈α∂use.␈α∂ We␈α∂will␈α∂often␈α⊂use␈α∂one
␈↓ ↓H␈↓argument␈αfunctions␈αsymbols␈αas␈αprefixes,␈αi.e.␈α without␈αbrackets,␈αjust␈αas␈α␈↓αa␈↓␈αand␈α␈↓αd␈↓␈αhave␈αbeen␈αused␈αup
␈↓ ↓H␈↓to now.

␈↓ ↓H␈↓␈↓αPredicate␈α∩symbols␈↓:␈α∩The␈α⊃letters␈α∩␈↓↓p␈↓,␈α∩␈↓↓q␈↓␈α⊃and␈α∩␈↓↓r␈↓␈α∩with␈α⊃or␈α∩without␈α∩subscripts␈α⊃are␈α∩used␈α∩as␈α⊃predicate
␈↓ ↓H␈↓symbols.␈α∂ We␈α∂will␈α∂also␈α∂use␈α∞the␈α∂LISP␈α∂predicate␈α∂symbol␈α∂␈↓αat␈↓␈α∞as␈α∂a␈α∂constant␈α∂predicate␈α∂symbol.␈α∞ The
␈↓ ↓H␈↓equality␈αsymbol␈α=␈α
is␈αalso␈αused␈α
as␈αan␈αinfix.␈α We␈α
suppose␈αthat␈αeach␈α
predicate␈αsymbol␈αtakes␈αthe␈α
same
␈↓ ↓H␈↓definite␈α∞number␈α∞of␈α∞arguments␈α∞each␈α∂time␈α∞it␈α∞is␈α∞used.␈α∞ Again␈α∂a␈α∞letter␈α∞may␈α∞be␈α∞used␈α∂with␈α∞differing
␈↓ ↓H␈↓numbers␈α
of␈α
arguments␈α
to␈α
represent␈α
different␈α
functions.␈α
 Infix␈α
and␈α
prefix␈α
notation␈α
will␈α
also␈αbe␈α
used
␈↓ ↓H␈↓where this is customary.

␈↓ ↓H␈↓␈↓ α_Next␈αwe␈αdefine␈αterms,␈αsentences,␈αfunction␈αexpressions␈αand␈αpredicate␈αexpressions␈αinductively.
␈↓ ↓H␈↓A␈αterm␈αis␈αan␈αexpression␈αwhose␈αvalue␈αwill␈αbe␈αan␈αobject␈αlike␈αan␈αS-expression␈αor␈αa␈αnumber␈αwhile␈αa
␈↓ ↓H␈↓sentence␈αhas␈αvalue␈αT␈αor␈αF.␈α Terms␈αare␈αused␈αin␈αmaking␈αsentences,␈αand␈αsentences␈αoccur␈αin␈αterms␈αso
␈↓ ↓H␈↓that␈α∪the␈α∪definitions␈α∪are␈α∪␈↓↓mutually␈α∪recursive␈↓␈α∪where␈α∪this␈α∪use␈α∪of␈α∪the␈α∪word␈α∪␈↓↓recursive␈↓␈α∪should␈α∪be
␈↓ ↓H␈↓distinguished␈α⊂from␈α⊂its␈α∂use␈α⊂in␈α⊂recursive␈α∂definitions␈α⊂of␈α⊂functions.␈α∂ Function␈α⊂expressions␈α⊂are␈α∂also
␈↓ ↓H␈↓involved in the mutual recursion.

␈↓ ↓H␈↓␈↓αTerms␈↓:␈α⊂Constants␈α⊃are␈α⊂terms,␈α⊃and␈α⊂variables␈α⊃are␈α⊂terms.␈α⊃ If␈α⊂␈↓↓f␈↓␈α⊃is␈α⊂a␈α⊃function␈α⊂expression␈α⊃taking␈α⊂␈↓↓n␈↓
␈↓ ↓H␈↓arguments,␈α
and␈α
␈↓↓t␈↓β1␈↓↓, ... ,t␈↓βn␈↓↓␈↓␈α
are␈α
terms,␈α
then␈α
␈↓↓f[t␈↓β1␈↓↓, ... ,t␈↓βn␈↓↓]␈↓␈α
is␈α
a␈α
term.␈α
 If␈α
␈↓↓p␈↓␈α
is␈α
a␈α
sentence␈α
and␈α
␈↓↓t␈↓β1␈↓↓␈↓␈αand␈α
␈↓↓t␈↓β2␈↓
␈↓ ↓H␈↓are␈α
terms,␈α∞then␈α
␈↓αif␈↓␈↓↓ p ␈↓αthen␈↓↓ t␈↓β1␈↓↓ ␈↓αelse␈↓↓ t␈↓β2␈↓␈α
is␈α∞a␈α
term.␈α
 We␈α∞soften␈α
the␈α
notation␈α∞by␈α
allowing␈α∞infix␈α
symbols
␈↓ ↓H␈↓where this is customary.

␈↓ ↓H␈↓␈↓αSentences␈↓:␈α⊂If␈α⊃␈↓↓p␈↓␈α⊂is␈α⊂a␈α⊃predicate␈α⊂expression␈α⊂taking␈α⊃␈↓↓n␈↓␈α⊂arguments␈α⊂and␈α⊃␈↓↓t␈↓β1␈↓↓, ... ,t␈↓βn␈↓↓␈↓␈α⊂are␈α⊃terms,␈α⊂then
␈↓ ↓H␈↓␈↓↓p[t␈↓β1␈↓↓, ... ,t␈↓βn␈↓↓]␈↓␈α∪is␈α∪a␈α∀sentence.␈α∪ Equality␈α∪is␈α∀also␈α∪used␈α∪as␈α∪an␈α∀infixed␈α∪predicate␈α∪symbol␈α∀to␈α∪form
␈↓ ↓H␈↓sentences,␈αi.e.␈α␈↓↓t␈↓β1␈↓↓ = t␈↓β2␈↓␈αis␈αa␈αsentence.␈α
 If␈α␈↓↓p␈↓␈αis␈αa␈αsentence,␈αthen␈α␈↓↓¬p␈↓␈α
is␈αalso␈αa␈αsentence.␈α If␈α␈↓↓p␈↓␈αand␈α
␈↓↓q␈↓␈αare
␈↓ ↓H␈↓sentences,␈α∃then␈α∃␈↓↓p∧q␈↓,␈α∃␈↓↓p∨q␈↓,␈α∃␈↓↓p⊃q␈↓,␈α∃and␈α∃␈↓↓p≡q␈↓␈α∃are␈α∀sentences.␈α∃ If␈α∃␈↓↓p␈↓,␈α∃␈↓↓q␈↓␈α∃and␈α∃␈↓↓r␈↓␈α∃are␈α∃sentences,␈α∀then
␈↓ ↓H␈↓␈↓αif␈↓␈↓↓ p ␈↓αthen␈↓↓ q ␈↓αelse␈↓↓ r␈↓␈α
is␈α
a␈α
sentence.␈α
 If␈α
␈↓↓x␈↓β1␈↓↓, ..., x␈↓βn␈↓↓␈↓␈α
are␈αvariables,␈α
and␈α
␈↓↓p␈↓␈α
is␈α
a␈α
term,␈α
then␈α␈↓↓∃x␈↓β1␈↓↓ ... x␈↓βn␈↓↓:t␈↓␈α
and
␈↓ ↓H␈↓␈↓↓∀x␈↓β1␈↓↓ ... x␈↓βn␈↓↓:t␈↓ are sentences.

␈↓ ↓H␈↓␈↓αFunction␈α
expressions␈↓:␈α∞A␈α
function␈α
symbol␈α∞is␈α
a␈α
function␈α∞expression.␈α
 If␈α
␈↓↓x␈↓β1␈↓↓, ... ,x␈↓βn␈↓↓␈↓␈α∞are␈α
variables
␈↓ ↓H␈↓and ␈↓↓t␈↓ is a term, then ␈↓↓[λx␈↓β1␈↓↓, ... ,x␈↓βn␈↓↓:t]␈↓ is a function expression.

␈↓ ↓H␈↓␈↓αPredicate␈αexpressions␈↓:␈αA␈αpredicate␈αsymbol␈αis␈αa␈αpredicate␈αexpression.␈α If␈α␈↓↓x␈↓β1␈↓↓, ... ,x␈↓βn␈↓↓␈↓␈αare␈αvariables
␈↓ ↓H␈↓and ␈↓↓p␈↓ is a sentence, then ␈↓↓[λx␈↓β1␈↓↓, ... ,x␈↓βn␈↓↓:p]␈↓ is a predicate expression.

␈↓ ↓H␈↓␈↓ α_An␈αoccurrence␈αof␈αa␈αvariable␈α␈↓↓x␈↓␈αis␈αcalled␈αbound␈αif␈αit␈αis␈αin␈αan␈αexpression␈αof␈αone␈αof␈αthe␈αforms
␈↓ ↓H␈↓␈↓↓[λx␈↓β1␈↓↓ ... x␈↓βn␈↓↓:t]␈↓,␈α
␈↓↓[λx␈↓β1␈↓↓ ... x␈↓βn␈↓↓:p]␈↓,␈α
␈↓↓[∀x␈↓β1␈↓↓ ... x␈↓βn␈↓↓:p]␈↓␈αor␈α
␈↓↓[∃x␈↓β1␈↓↓ ... x␈↓βn␈↓↓:p]␈↓␈α
where␈α␈↓↓x␈↓␈α
is␈α
one␈αof␈α
the␈α
numbered␈α␈↓↓x␈↓'s.␈α
 If
␈↓ ↓H␈↓not bound an occurrence is called free.
␈↓ ↓H␈↓␈↓ ¬oCHAPTER I␈↓ 93


␈↓ ↓H␈↓␈↓ α_The␈α␈↓↓semantics␈↓␈αof␈αfirst␈αorder␈αlogic␈αconsists␈αof␈αthe␈αrules␈αthat␈αdetermine␈αwhether␈αa␈αsentence␈αis
␈↓ ↓H␈↓true␈αor␈αfalse.␈α However,␈αthe␈αtruth␈αor␈αfalsity␈αof␈αa␈αsentence␈αis␈αrelative␈αto␈αthe␈αinterpretation␈αassigned
␈↓ ↓H␈↓to␈α
the␈α
constants,␈α
the␈α∞function␈α
and␈α
predicate␈α
symbols␈α
and␈α∞the␈α
free␈α
variables␈α
of␈α
the␈α∞formula.␈α
 We
␈↓ ↓H␈↓proceed as follows:

␈↓ ↓H␈↓␈↓ α_We␈αbegin␈αby␈αchoosing␈αa␈αdomain.␈α In␈αmost␈αcases,␈αthe␈αdomain␈αwill␈αinclude␈αthe␈αS-expressions,
␈↓ ↓H␈↓and␈αany␈αS-expression␈α
constants␈αappearing␈αin␈αthe␈α
formula␈αstand␈αfor␈α
themselves.␈α We␈αwill␈αallow␈α
for
␈↓ ↓H␈↓the␈α
possibility␈α
that␈αother␈α
objects␈α
than␈αS-expressions␈α
exist,␈α
and␈αsome␈α
constants␈α
may␈αdesignate␈α
them.
␈↓ ↓H␈↓A␈αspecial␈αconstant␈αsymbol␈αqw␈αis␈αused␈αfor␈αthe␈αvalue␈αof␈αthe␈αfunction␈αdefined␈αby␈αa␈αLisp␈αprogram␈αin
␈↓ ↓H␈↓case the computation doesn't terminate; its use requires a justification that will be given later.

␈↓ ↓H␈↓␈↓ α_Each␈αfunction␈αor␈α
predicate␈αsymbol␈αis␈α
assigned␈αa␈αfunction␈αor␈α
predicate␈αon␈αthe␈α
domain.␈α We
␈↓ ↓H␈↓will␈α∞normally␈α∂assign␈α∞to␈α∂the␈α∞basic␈α∂LISP␈α∞function␈α∂and␈α∞predicate␈α∂symbols␈α∞the␈α∂corresponding␈α∞basic
␈↓ ↓H␈↓LISP␈α∞functions␈α∞and␈α∞predicates.␈α∞ Each␈α∞variable␈α∞appearing␈α∞free␈α∞in␈α∞a␈α∞sentence␈α∞is␈α∞also␈α∞assigned␈α∞an
␈↓ ↓H␈↓element␈α⊂of␈α∂the␈α⊂domain.␈α∂ All␈α⊂these␈α⊂assignments␈α∂constitute␈α⊂an␈α∂interpretation,␈α⊂and␈α∂the␈α⊂truth␈α⊂of␈α∂a
␈↓ ↓H␈↓sentence is relative to the interpretation.

␈↓ ↓H␈↓␈↓ α_The␈α⊂truth␈α∂of␈α⊂a␈α∂sentence␈α⊂is␈α⊂determined␈α∂from␈α⊂the␈α∂values␈α⊂of␈α∂its␈α⊂constituents␈α⊂by␈α∂evaluating
␈↓ ↓H␈↓successively␈α∞larger␈α∞subexpressions.␈α
 The␈α∞rules␈α∞for␈α
handling␈α∞functions␈α∞and␈α∞predicates,␈α
conditional
␈↓ ↓H␈↓expressions,␈αequality,␈αand␈αBoolean␈αexpressions␈αare␈αexactly␈αthe␈αsame␈αas␈αthose␈αwe␈αhave␈αused␈αin␈αthe
␈↓ ↓H␈↓previous chapters.  We need only explain quantifiers:

␈↓ ↓H␈↓␈↓ α_␈↓↓∀x␈↓β1␈↓↓ ... x␈↓βn␈↓↓:e␈↓␈αis␈αassigned␈αtrue␈αif␈αand␈αonly␈αif␈α␈↓↓e␈↓␈αis␈αassigned␈αtrue␈αfor␈αall␈αassignments␈αof␈αelements
␈↓ ↓H␈↓of␈αthe␈αdomain␈αto␈αthe␈α␈↓↓x␈↓'s.␈α If␈α␈↓↓e␈↓␈αhas␈αfree␈αvariables␈αthat␈αare␈αnot␈αamong␈αthe␈α␈↓↓x␈↓'s,␈αthen␈αthe␈αtruth␈αof␈αthe
␈↓ ↓H␈↓sentence␈α
depends␈α
on␈α
the␈αvalues␈α
assigned␈α
to␈α
these␈αremaining␈α
free␈α
variables.␈α
 ␈↓↓∃x␈↓β1␈↓↓ ... x␈↓βn␈↓↓:e␈↓␈αis␈α
assigned
␈↓ ↓H␈↓true␈αif␈αand␈αonly␈αif␈α␈↓↓e␈↓␈αis␈αassigned␈αtrue␈αfor␈α␈↓↓some␈↓␈αassignment␈αof␈αvalues␈αin␈αthe␈αdomain␈αto␈αthe␈α␈↓↓x␈↓'s.␈α Free
␈↓ ↓H␈↓variables are handled just as before.

␈↓ ↓H␈↓␈↓ α_␈↓↓λx␈↓β1␈↓↓ ... x␈↓βn␈↓↓:u␈↓␈α⊃is␈α⊃assigned␈α⊂a␈α⊃function␈α⊃or␈α⊂predicate␈α⊃according␈α⊃to␈α⊂whether␈α⊃␈↓↓u␈↓␈α⊃is␈α⊂a␈α⊃term␈α⊃or␈α⊂a
␈↓ ↓H␈↓sentence.␈α The␈αvalue␈αof␈α␈↓↓[λx␈↓β1␈↓↓ ... x␈↓βn␈↓↓:u][t␈↓β1␈↓↓,...,t␈↓βn␈↓↓]␈↓␈αis␈αobtained␈αby␈αevaluating␈αthe␈α␈↓↓t␈↓'s␈αand␈αusing␈αthese
␈↓ ↓H␈↓values␈αas␈α
values␈αof␈α
the␈α␈↓↓x␈↓'s␈α
in␈αthe␈α
evaluation␈αof␈α␈↓↓u␈↓.␈α
 If␈α␈↓↓u␈↓␈α
has␈αfree␈α
variables␈αin␈α
addition␈αto␈α
the␈α␈↓↓x␈↓'s,
␈↓ ↓H␈↓the function assigned will depend on them too.

␈↓ ↓H␈↓␈↓ α_Those␈α
who␈αare␈α
familiar␈αwith␈α
the␈α
lambda␈αcalculus␈α
should␈αnote␈α
that␈α
λ␈αis␈α
being␈αused␈α
here␈αin␈α
a
␈↓ ↓H␈↓very␈α
limited␈α
way.␈α Namely,␈α
the␈α
variables␈αin␈α
a␈α
lambda-expression␈α
take␈αonly␈α
elements␈α
of␈αthe␈α
domain
␈↓ ↓H␈↓as␈α⊂values,␈α⊂whereas␈α∂the␈α⊂essence␈α⊂of␈α∂the␈α⊂lambda␈α⊂calculus␈α∂is␈α⊂that␈α⊂they␈α∂take␈α⊂arbitrary␈α⊂functions␈α∂as
␈↓ ↓H␈↓values.  We may call these restricted lambda expressions ␈↓↓first order lambdas␈↓.



␈↓ ↓H␈↓2.  ␈↓αConditional forms.␈↓


␈↓ ↓H␈↓␈↓ α_All the properties we shall use of conditional forms follow from the relation

␈↓ ↓H␈↓␈↓ α_␈↓↓[p ⊃ [␈↓αif␈↓↓ p ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b] = a] ∧ [¬p ⊃ [␈↓αif␈↓↓ p ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b] = b]␈↓.

␈↓ ↓H␈↓␈↓ α_It is worthwhile to list separately some properties of conditional forms.

␈↓ ↓H␈↓␈↓ α_First we have the obvious
␈↓ ↓H␈↓␈↓ ¬oCHAPTER I␈↓ 94


␈↓ ↓H␈↓␈↓ α_␈↓↓␈↓αif␈↓↓ T ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b = a␈↓

␈↓ ↓H␈↓and

␈↓ ↓H␈↓␈↓ α_␈↓↓␈↓αif␈↓↓ F ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b = b␈↓.

␈↓ ↓H␈↓␈↓ α_Next we have a ␈↓↓distributive law␈↓ for functions applied to conditional forms, namely

␈↓ ↓H␈↓␈↓ α_␈↓↓f[␈↓αif␈↓↓ p ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b] = ␈↓αif␈↓↓ p ␈↓αthen␈↓↓ f[a] ␈↓αelse␈↓↓ f[b]␈↓.

␈↓ ↓H␈↓This␈α
applies␈αto␈α
predicates␈αas␈α
well␈αas␈α
functions␈αand␈α
can␈α
also␈αbe␈α
used␈αwhen␈α
one␈αof␈α
the␈αarguments␈α
of
␈↓ ↓H␈↓a␈αfunction␈αof␈αseveral␈αarguments␈αis␈αa␈αconditional␈αform.␈α It␈αalso␈αapplies␈αwhen␈αone␈αof␈αthe␈αterms␈αof␈αa
␈↓ ↓H␈↓conditional form is itself a conditional form.

␈↓ ↓H␈↓Thus

␈↓ ↓H␈↓␈↓ α_␈↓↓␈↓αif␈↓↓ [␈↓αif␈↓↓ p ␈↓αthen␈↓↓ q ␈↓αelse␈↓↓ r] ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b = ␈↓αif␈↓↓ p ␈↓αthen␈↓↓ [␈↓αif␈↓↓ q ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b] ␈↓αelse␈↓↓ [␈↓αif␈↓↓ r ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b]␈↓

␈↓ ↓H␈↓and

␈↓ ↓H␈↓␈↓ α_␈↓↓␈↓αif␈↓↓ p ␈↓αthen␈↓↓ [␈↓αif␈↓↓ q ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b] ␈↓αelse␈↓↓ c = ␈↓αif␈↓↓ q ␈↓αthen␈↓↓ [␈↓αif␈↓↓ p ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ c] ␈↓αelse␈↓↓ [␈↓αif␈↓↓ p ␈↓αthen␈↓↓ b ␈↓αelse␈↓↓ c]␈↓.

␈↓ ↓H␈↓␈↓ α_When␈αthe␈αexpressions␈αfollowing␈α␈↓αthen␈↓␈αand␈α␈↓αelse␈↓␈αare␈αsentences,␈αthen␈αthe␈αconditional␈αform␈αcan
␈↓ ↓H␈↓be replaced by a sentence according to

␈↓ ↓H␈↓␈↓ α_␈↓↓[␈↓αif␈↓↓ p ␈↓αthen␈↓↓ q ␈↓αelse␈↓↓ r] ≡ [p ∧ q] ∨ [¬p ∧ r]␈↓.

␈↓ ↓H␈↓These␈α
two␈α
rules␈α
permit␈αeliminating␈α
conditional␈α
forms␈α
from␈αsentences␈α
by␈α
first␈α
using␈αdistributivity
␈↓ ↓H␈↓to␈αmove␈αthe␈αconditionals␈αto␈αthe␈αoutside␈αof␈αany␈αfunctions␈αand␈αthen␈αreplacing␈αthe␈αconditional␈αform
␈↓ ↓H␈↓by a Boolean expression.

␈↓ ↓H␈↓␈↓ α_Note␈α
that␈α
the␈α
elimination␈α
of␈α
conditional␈α
forms␈αmay␈α
increase␈α
the␈α
size␈α
of␈α
a␈α
sentence,␈αbecause␈α
␈↓↓p␈↓
␈↓ ↓H␈↓occurs␈αtwice␈αin␈αthe␈αright␈αhand␈αside␈αof␈αthe␈αabove␈αequivalence.␈α In␈αthe␈αmost␈αunfavorable␈αcase,␈α␈↓↓p␈↓␈αis
␈↓ ↓H␈↓dominates␈α∩the␈α⊃size␈α∩of␈α⊃the␈α∩expression␈α⊃so␈α∩that␈α⊃writing␈α∩it␈α⊃twice␈α∩almost␈α⊃doubles␈α∩the␈α⊃size␈α∩of␈α⊃the
␈↓ ↓H␈↓expression.

␈↓ ↓H␈↓␈↓ α_Suppose␈αthat␈α␈↓↓a␈↓␈αand␈α␈↓↓b␈↓␈αin␈α␈↓↓␈↓αif␈↓↓ p ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b␈↓␈αare␈αexpressions␈αthat␈αmay␈αcontain␈αthe␈αsentence␈α␈↓↓p␈↓.
␈↓ ↓H␈↓Occurrences␈α
of␈α
␈↓↓p␈↓␈α
in␈α
␈↓↓a␈↓␈α
can␈αbe␈α
replaced␈α
by␈α
T,␈α
and␈α
occurrences␈α
of␈α␈↓↓p␈↓␈α
in␈α
␈↓↓b␈↓␈α
can␈α
be␈α
replaced␈α
by␈αF.␈α
 This
␈↓ ↓H␈↓follows from the fact that ␈↓↓a␈↓ is only evaluated if ␈↓↓p␈↓ is true and ␈↓↓b␈↓ is evaluated only if ␈↓↓p␈↓ is false.

␈↓ ↓H␈↓␈↓ α_This␈α∂leads␈α⊂to␈α∂a␈α⊂strengthened␈α∂form␈α⊂of␈α∂the␈α⊂law␈α∂of␈α⊂replacement␈α∂of␈α⊂equals␈α∂by␈α⊂equals.␈α∂ The
␈↓ ↓H␈↓ordinary␈αform␈αof␈αthe␈αlaw␈αsays␈αthat␈αif␈αwe␈αhave␈α␈↓↓e = e'␈↓,␈αthen␈αwe␈αcan␈αreplace␈αany␈αoccurrence␈αof␈α
␈↓↓e␈↓␈αin
␈↓ ↓H␈↓an␈α∞expression␈α∞by␈α
an␈α∞occurrence␈α∞of␈α∞␈↓↓e'␈↓.␈α
 However,␈α∞if␈α∞we␈α
want␈α∞to␈α∞replace␈α∞␈↓↓e␈↓␈α
by␈α∞␈↓↓e'␈↓␈α∞within␈α∞␈↓↓a␈↓␈α
within
␈↓ ↓H␈↓␈↓αif␈↓␈↓↓ p ␈↓αthen␈↓↓ a ␈↓αelse␈↓↓ b␈↓,␈α
then␈α
we␈α
need␈α
only␈α
prove␈α
␈↓↓p ⊃ e =e'␈↓,␈α
and␈α
to␈α
make␈α
the␈α
replacement␈α
within␈α∞␈↓↓b␈↓␈α
we
␈↓ ↓H␈↓need only prove ␈↓↓¬p ⊃ e = e'␈↓.

␈↓ ↓H␈↓␈↓ α_More␈α
facts␈α
about␈α
conditional␈α
forms␈α
are␈αgiven␈α
in␈α
(McCarthy␈α
1963a)␈α
including␈α
a␈αdiscussion␈α
of
␈↓ ↓H␈↓canonical␈α
forms␈αthat␈α
parallels␈αthe␈α
canonical␈αforms␈α
of␈αBoolean␈α
forms.␈α Any␈α
question␈αof␈α
equivalence
␈↓ ↓H␈↓of conditional forms is decidable by truth tables analogously to the decidability of Boolean forms.
␈↓ ↓H␈↓␈↓ ¬oCHAPTER I␈↓ 95


␈↓ ↓H␈↓3.  ␈↓αLambda-expressions.␈↓


␈↓ ↓H␈↓␈↓ α_The␈α∪only␈α∩rule␈α∪required␈α∩for␈α∪handling␈α∪lambda-expressions␈α∩in␈α∪first␈α∩order␈α∪logic␈α∪is␈α∩called
␈↓ ↓H␈↓␈↓↓lambda-conversion␈↓, essentially

␈↓ ↓H␈↓␈↓ α_␈↓↓[λx:e][a] =␈↓ <the result of substituting ␈↓↓e␈↓ for ␈↓↓x␈↓ in ␈↓↓a␈↓>.

␈↓ ↓H␈↓As examples of this rule, we have

␈↓ ↓H␈↓␈↓ α_␈↓↓[λx:␈↓αa␈↓↓ x . y][u . v] = [␈↓αa␈↓↓ [u . v]] . y␈↓.

␈↓ ↓H␈↓However,␈αa␈α
complication␈αrequires␈α
modifying␈αthe␈α
rule.␈α Namely,␈α
we␈αcan't␈α
substitute␈αfor␈α
a␈αvariable␈α
␈↓↓x␈↓
␈↓ ↓H␈↓an␈αexpression␈α␈↓↓e␈↓␈αthat␈αhas␈αa␈αfree␈αvariable␈α␈↓↓y␈↓␈αinto␈αa␈αcontext␈αin␈αwhich␈α␈↓↓y␈↓␈αis␈αbound.␈α Thus␈αit␈αwould␈αbe
␈↓ ↓H␈↓wrong␈α
to␈α
substitute␈α
␈↓↓y + z␈↓␈α∞for␈α
␈↓↓x␈↓␈α
in␈α
␈↓↓∀y:[x + y = z]␈↓␈α
or␈α∞into␈α
the␈α
term␈α
␈↓↓[λy:x + y][u + v]␈↓.␈α∞ Before␈α
doing
␈↓ ↓H␈↓the␈αsubstitution,␈αthe␈αvariable␈α␈↓↓y␈↓␈αwould␈αhave␈αto␈αbe␈αreplaced␈αin␈αall␈αits␈αbound␈αoccurrences␈αby␈αa␈αfresh
␈↓ ↓H␈↓variable.

␈↓ ↓H␈↓␈↓ α_Lambda-expressions␈α∀can␈α∀always␈α∃be␈α∀eliminated␈α∀from␈α∃sentences␈α∀and␈α∀terms␈α∃by␈α∀lambda-
␈↓ ↓H␈↓conversion,␈αbut␈αthe␈αexpression␈αmay␈α
increase␈αgreatly␈αin␈αlength␈αif␈α
a␈αlengthy␈αterm␈αreplaces␈αa␈α
variable
␈↓ ↓H␈↓that␈α∞occurs␈α∞more␈α∞than␈α∞once␈α∞in␈α
␈↓↓e␈↓.␈α∞ It␈α∞is␈α∞easy␈α∞to␈α∞make␈α
an␈α∞expression␈α∞of␈α∞length␈α∞␈↓↓n␈↓␈α∞whose␈α∞length␈α
is
␈↓ ↓H␈↓increased to 2␈↓∧n␈↓ by converting its ␈↓↓n␈↓ nested lambda-expressions.



␈↓ ↓H␈↓4.  ␈↓αAlgebraic axioms for S-expressions and lists.␈↓


␈↓ ↓H␈↓␈↓ α_The␈α∂algebraic␈α∞facts␈α∂about␈α∞S-expressions␈α∂are␈α∞expressed␈α∂by␈α∞the␈α∂following␈α∞sentences␈α∂of␈α∞first
␈↓ ↓H␈↓order logic:

␈↓ ↓H␈↓␈↓ α_␈↓↓∀x.(issexp x ⊃ ␈↓αat␈↓↓ x ∨ (issexp ␈↓αa␈↓↓ x ∧ issexp ␈↓αd␈↓↓ x ∧ x = (␈↓αa␈↓↓ x . ␈↓αd␈↓↓ x)))␈↓

␈↓ ↓H␈↓and

␈↓ ↓H␈↓␈↓ α_␈↓↓∀x y.(issexp x ∧ issexp y ⊃ issexp(x.y) ∧ ¬␈↓αat␈↓↓(x.y) ∧ x = ␈↓αa␈↓↓(x.y) ∧ y = ␈↓αd␈↓↓(x.y))␈↓.

␈↓ ↓H␈↓Here␈α␈↓↓issexp␈αe␈↓␈αasserts␈αthat␈αthe␈αobject␈α␈↓↓e␈↓␈αis␈αan␈αS-expression␈αso␈αthat␈αthe␈αsentences␈αused␈αin␈αproving␈αa
␈↓ ↓H␈↓particular␈α
program␈αcorrect␈α
can␈αinvolve␈α
other␈αkinds␈α
of␈α
entities␈αas␈α
well.␈α If␈α
we␈αcan␈α
assume␈α
that␈αall
␈↓ ↓H␈↓objects␈αare␈αS-expressions␈αor␈αcan␈αdeclare␈αcertain␈αvariables␈αas␈αranging␈αonly␈αover␈αS-expressions,␈αwe
␈↓ ↓H␈↓can simplify the axioms to

␈↓ ↓H␈↓␈↓ α_␈↓↓∀x.[␈↓αat␈↓↓ x ∨ x = [␈↓αa␈↓↓ x . ␈↓αd␈↓↓ x]]␈↓

␈↓ ↓H␈↓and

␈↓ ↓H␈↓␈↓ α_␈↓↓∀x y.[¬␈↓αat␈↓↓[x.y] ∧ x = ␈↓αa␈↓↓[x.y] ∧ y = ␈↓αd␈↓↓[x.y]]␈↓.

␈↓ ↓H␈↓␈↓ α_The algebraic facts about lists are expressed by the following sentences of first order logic:
␈↓ ↓H␈↓␈↓ ¬oCHAPTER I␈↓ 96


␈↓ ↓H␈↓␈↓ α_␈↓↓∀x. islist x ⊃ x = ␈↓NIL␈↓↓ ∨ islist ␈↓αd␈↓↓ x␈↓,

␈↓ ↓H␈↓␈↓ α_␈↓↓∀x y. islist y ⊃ islist[x . y]␈↓,

␈↓ ↓H␈↓␈↓ α_␈↓↓∀x y. islist y ⊃ ␈↓αa␈↓↓[x . y] = x ∧ ␈↓αd␈↓↓[x.y] = y␈↓.

␈↓ ↓H␈↓We␈αcan␈α
rarely␈αassume␈α
that␈αeverything␈α
is␈αa␈αlist,␈α
because␈αthe␈α
lists␈αusually␈α
contain␈αatoms␈α
which␈αare
␈↓ ↓H␈↓not themselves lists.

␈↓ ↓H␈↓␈↓ α_These␈α
axioms␈α
are␈α
analogous␈α
to␈α
the␈αalgebraic␈α
part␈α
of␈α
Peano's␈α
axioms␈α
for␈α
the␈αnon-negative
␈↓ ↓H␈↓integers.␈α The␈αanalogy␈αcan␈αbe␈αmade␈αclear␈αif␈αwe␈αwrite␈αPeano's␈αaxioms␈αusing␈α␈↓↓n'␈↓␈αfor␈αthe␈αsuccessor␈α
of
␈↓ ↓H␈↓␈↓↓n␈↓ and ␈↓↓n␈↓∧-␈↓ for the predecessor of ␈↓↓n␈↓.  Peano's algebraic axioms then become

␈↓ ↓H␈↓␈↓ α_␈↓↓∀n: n' ≠ 0␈↓,

␈↓ ↓H␈↓␈↓ α_␈↓↓∀n: (n')␈↓∧-␈↓↓ = n␈↓,

␈↓ ↓H␈↓and

␈↓ ↓H␈↓␈↓ α_␈↓↓∀n: n ≠ 0 ⊃ (n␈↓∧-␈↓↓)' = n␈↓.

␈↓ ↓H␈↓Integers␈αspecialize␈α lists␈αif␈αwe␈αidentify␈α0␈αwith␈αNIL␈α
and␈αassume␈αthat␈αthere␈αis␈αonly␈αone␈αobject␈α(say␈α
1)
␈↓ ↓H␈↓that can serve as a list element.  Then ␈↓↓n' = cons[1,n]␈↓, and ␈↓↓n␈↓∧-␈↓↓ = ␈↓αd␈↓↓ n␈↓.

␈↓ ↓H␈↓␈↓ α_Clearly␈α∞S-expressions␈α
and␈α∞lists␈α
satisfy␈α∞the␈α∞axioms␈α
given␈α∞for␈α
them,␈α∞but␈α∞unfortunately␈α
these
␈↓ ↓H␈↓algebraic␈α∞axioms␈α∞are␈α∞insufficient␈α∞to␈α∞characterize␈α∂them.␈α∞ For␈α∞example,␈α∞consider␈α∞a␈α∞domain␈α∂of␈α∞one
␈↓ ↓H␈↓element ␈↓↓a␈↓ satisfying

␈↓ ↓H␈↓␈↓ α_␈↓↓␈↓αa␈↓↓ a = ␈↓αd␈↓↓ a = a . a = a␈↓.

␈↓ ↓H␈↓It␈αsatisfies␈αthe␈αalgebraic␈αaxioms␈αfor␈αS-expressions.␈α We␈αcan␈αexclude␈αit␈αby␈αan␈αaxiom␈α␈↓↓∀x.(␈↓αa␈↓↓␈αx␈α≠␈αx)␈↓,
␈↓ ↓H␈↓but␈αthis␈αwon't␈α
exclude␈αother␈αcircular␈αlist␈α
structures␈αthat␈αeventually␈αreturn␈α
to␈αthe␈αsame␈α
element␈αby
␈↓ ↓H␈↓some␈α∂␈↓αa-d␈↓␈α∂chain.␈α∂ Actually␈α∞we␈α∂want␈α∂to␈α∂exclude␈α∂all␈α∞infinite␈α∂chains,␈α∂because␈α∂most␈α∂LISP␈α∞programs
␈↓ ↓H␈↓won't␈αterminate␈αunless␈αevery␈α␈↓αa-d␈↓␈αchain␈αeventually␈αterminates␈αin␈αan␈αatom.␈α This␈αcannot␈αbe␈αdone␈αby
␈↓ ↓H␈↓any finite set of axioms.



␈↓ ↓H␈↓5.  ␈↓αAxiom schemas of induction.␈↓


␈↓ ↓H␈↓␈↓ α_In␈αorder␈αto␈αexclude␈αcircular␈αand␈αinfinite␈αlist␈αstructures␈αwe␈αneed␈αaxiom␈αschemas␈αof␈αinduction
␈↓ ↓H␈↓analogous to Peano's for the integers.  Peano's induction schema is ordinarily written

␈↓ ↓H␈↓␈↓ α_␈↓↓P(0) ∧ ∀n:(P(n) ⊃ P(n')) ⊃ ∀n:P(n)␈↓.

␈↓ ↓H␈↓Here␈α␈↓↓P(n)␈↓␈αis␈αan␈αarbitrary␈α
predicate␈αof␈αintegers,␈αand␈αwe␈α
get␈αparticular␈αinstances␈αof␈αthe␈α
schema␈αby
␈↓ ↓H␈↓substituting␈αparticular␈αpredicates.␈α It␈αis␈αcalled␈αan␈αaxiom␈αschema␈αrather␈αthan␈αan␈αaxiom,␈αbecause␈αwe
␈↓ ↓H␈↓consider␈α∂the␈α∂schema,␈α∂which␈α∂is␈α∂not␈α∂properly␈α⊂a␈α∂sentence␈α∂of␈α∂first␈α∂order␈α∂logic,␈α∂as␈α∂standing␈α⊂for␈α∂the
␈↓ ↓H␈↓␈↓ ¬oCHAPTER I␈↓ 97


␈↓ ↓H␈↓infinite␈α∩collection␈α∩of␈α∩axioms␈α∩that␈α∩arise␈α∩from␈α∩it␈α∩by␈α∩substituting␈α∩all␈α∩possible␈α∩predicates␈α∪for␈α∩␈↓↓P␈↓.
␈↓ ↓H␈↓Peano's induction schema can also be written

␈↓ ↓H␈↓␈↓ α_␈↓↓∀n:(n = 0 ∨ P(n␈↓∧-␈↓↓) ⊃ P(n)) ⊃ ∀n:P(n)␈↓,

␈↓ ↓H␈↓and the equivalence of the two forms is easily proved.

␈↓ ↓H␈↓␈↓ α_The S-expression analog of this second form is

␈↓ ↓H␈↓␈↓ α_␈↓↓∀x:[issexp x ⊃ [␈↓αat␈↓↓ x ∨ P[␈↓αa␈↓↓ x] ∧ P[␈↓αd␈↓↓ x] ⊃ P[x]]] ⊃ ∀x:[issexp x ⊃ P[x]]␈↓,

␈↓ ↓H␈↓or, declaring the variable ␈↓↓x␈↓ to range over S-expressions,

␈↓ ↓H␈↓␈↓ α_␈↓↓∀x:[␈↓αat␈↓↓ x ∨ P[␈↓αa␈↓↓ x] ∧ P[␈↓αd␈↓↓ x] ⊃ P[x]] ⊃ ∀x:P[x]␈↓.

␈↓ ↓H␈↓␈↓ α_The corresponding axiom schema for lists is

␈↓ ↓H␈↓␈↓ α_␈↓↓∀u:[␈↓αn␈↓↓ u ∨ P[␈↓αd␈↓↓ u] ⊃ P[u]] ⊃ ∀u:P[u]␈↓.

␈↓ ↓H␈↓␈↓ α_These␈α∂schemas␈α∞are␈α∂called␈α∞principles␈α∂of␈α∞␈↓↓structural␈α∂induction␈↓,␈α∞since␈α∂the␈α∞induction␈α∂is␈α∂on␈α∞the
␈↓ ↓H␈↓structure of the entities involved.

␈↓ ↓H␈↓␈↓ α_Even␈αthe␈αaxiom␈αschemas␈αdon't␈αassure␈αus␈αthat␈αthe␈αonly␈αdomain␈αsatisfying␈αthe␈αaxioms␈αis␈αthat
␈↓ ↓H␈↓of␈αthe␈αintegers␈αor␈αthe␈αS-expressions␈αas␈αthe␈α
case␈αmay␈αbe.␈α Any␈αfirst␈αorder␈αtheory␈αwhose␈αaxioms␈α
can
␈↓ ↓H␈↓be␈α
given␈αeffectively␈α
admits␈α
the␈αso-called␈α
␈↓↓non-standard␈αmodels␈↓.␈α
 However,␈α
it␈αseems␈α
likely␈α
that␈αthe
␈↓ ↓H␈↓non-standard␈α
models␈α
of␈α
S-expressions,␈α
like␈α
the␈α
non-standard␈α
models␈α
of␈α
integers,␈α
will␈α
agree␈αwith
␈↓ ↓H␈↓the standard model for sentences of practical interest.



␈↓ ↓H␈↓6.  ␈↓αProofs by structural induction.␈↓


␈↓ ↓H␈↓␈↓ α_Recall that the operation that appends two lists is defined by

␈↓ ↓H␈↓1)␈↓ α8 ␈↓↓u * v ← ␈↓αif␈↓↓ n u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αa␈↓↓ u . [␈↓αd␈↓↓ u * v]␈↓.

␈↓ ↓H␈↓Assume␈αthat␈α␈↓↓u␈α*␈αv␈↓␈αis␈αdefined␈αfor␈αall␈α␈↓↓u␈↓␈αand␈α␈↓↓v␈↓,␈αi.e.␈αthe␈αcomputation␈αdescribed␈αabove␈αterminates␈αfor
␈↓ ↓H␈↓all ␈↓↓u␈↓ and ␈↓↓v␈↓; we will show how to prove it later.  Then we can replace (1) by the sentence

␈↓ ↓H␈↓2)␈↓ α8 ␈↓↓∀u v:[islist u ∧ islist v ⊃ [u * v = ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αa␈↓↓ u . [␈↓αd␈↓↓ u * v]]]␈↓.

␈↓ ↓H␈↓Now␈α⊂suppose␈α⊃we␈α⊂would␈α⊃like␈α⊂to␈α⊃prove␈α⊂␈↓↓∀v:[␈↓NIL␈↓↓␈α⊃*␈α⊂v␈α⊂=␈α⊃v]␈↓.␈α⊂ This␈α⊃is␈α⊂quite␈α⊃trivial;␈α⊂we␈α⊃need␈α⊂only
␈↓ ↓H␈↓substitute NIL for ␈↓↓x␈↓ in (2), getting

␈↓ ↓H␈↓␈↓ α>␈↓↓␈↓NIL␈↓↓ * v ␈↓ β( = ␈↓αif␈↓↓ n ␈↓NIL␈↓↓ ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ a ␈↓NIL␈↓↓ . [␈↓αd␈↓↓ ␈↓NIL␈↓↓ * v]

␈↓ ↓H␈↓↓␈↓ β( = v␈↓.
␈↓ ↓H␈↓␈↓ ¬oCHAPTER I␈↓ 98


␈↓ ↓H␈↓Next␈αconsider␈αproving␈α␈↓↓∀u:[u␈α*␈α␈↓NIL␈↓↓␈α=␈αu]␈↓.␈α This␈αcannot␈αbe␈αdone␈αby␈αsimple␈αsubstitution,␈αbut␈αit␈αcan
␈↓ ↓H␈↓be done as follows:  First substitute ␈↓↓λu:[u * ␈↓NIL␈↓↓ = u]␈↓ for ␈↓↓P␈↓ in the induction schema

␈↓ ↓H␈↓␈↓ α_␈↓↓∀u:[islist u ⊃ [␈↓αn␈↓↓ u ∨ P[␈↓αd␈↓↓ u] ⊃ P[u]]] ⊃ ∀u:[islist u ⊃ P[u]]␈↓,

␈↓ ↓H␈↓getting

␈↓ ↓H␈↓␈↓ α_␈↓↓∀u:[islist␈αu␈α⊃␈α[␈↓αn␈↓↓␈αu␈α∨␈α[λu:␈αu␈α
*␈α␈↓NIL␈↓↓␈α=␈αu][␈↓αd␈↓↓␈αu]␈α⊃␈αλu:[u␈α*␈α
␈↓NIL␈↓↓␈α=␈αu][u]]]␈α⊃␈α∀u:[islist␈αu␈α⊃␈αλu:[u␈α
*
␈↓ ↓H␈↓↓␈↓NIL␈↓↓ = u][u]]␈↓.

␈↓ ↓H␈↓Carrying out the indicated lambda conversions makes this

␈↓ ↓H␈↓3)␈↓ α8 ␈↓↓∀u:[islist u ⊃ [␈↓αn␈↓↓ u ∨ ␈↓αd␈↓↓ u * ␈↓NIL␈↓↓ = ␈↓αd␈↓↓ u] ⊃ u * ␈↓NIL␈↓↓ = u] ⊃ ∀u:[islist u ⊃ u * ␈↓NIL␈↓↓ = u]␈↓.

␈↓ ↓H␈↓␈↓ α_Next␈α
we␈α
must␈α
use␈α
the␈α
recursive␈α
definition␈α
of␈α
␈↓↓u*v␈↓.␈α
 There␈α
are␈α
two␈α
cases␈α
according␈αto␈α
whether
␈↓ ↓H␈↓␈↓αn␈↓␈α␈↓↓u␈↓␈αor␈αnot.␈α In␈αthe␈αfirst␈αcase,␈αwe␈αsubstitute␈αNIL␈αfor␈α␈↓↓v␈↓␈αand␈αget␈αNIL*NIL = NIL,␈αand␈αin␈αthe␈αsecond
␈↓ ↓H␈↓case␈α
we␈α
use␈α
the␈α
hypothesis␈α
␈↓αd␈↓ u * NIL = ␈↓αd␈↓ u␈α
and␈α∞the␈α
third␈α
algebraic␈α
axiom␈α
for␈α
lists␈α
to␈α∞make␈α
the
␈↓ ↓H␈↓simplification

␈↓ ↓H␈↓4)␈↓ α8 ␈↓↓␈↓αa␈↓↓ u . [␈↓αd␈↓↓ u * ␈↓NIL␈↓↓] = ␈↓αa␈↓↓ u . ␈↓αd␈↓↓ u = u.␈↓

␈↓ ↓H␈↓Combining␈α
the␈α
cases␈α
gives␈α
the␈α
hypothesis␈α
of␈α(3)␈α
and␈α
hence␈α
its␈α
conclusion,␈α
which␈α
is␈α
the␈αstatement␈α
to
␈↓ ↓H␈↓be proved.



␈↓ ↓H␈↓7.  ␈↓αFirst Order Theory of Partial Functions␈↓


␈↓ ↓H␈↓␈↓ α_In␈αthe␈αprevious␈α
section␈αwe␈αproved␈α
facts␈αabout␈αLisp␈α
functions␈αstarting␈αfrom␈α
the␈αassumption
␈↓ ↓H␈↓that␈α
their␈αcomputation␈α
terminated␈α
for␈αall␈α
values␈αof␈α
the␈α
arguments.␈α This␈α
enabled␈αus␈α
to␈α
write␈αthe
␈↓ ↓H␈↓definition␈α
as␈αa␈α
sentence␈α
of␈αfirst␈α
order␈αlogic.␈α
 However,␈α
when␈αwe␈α
write␈αdown␈α
a␈α
recursive␈αfunction
␈↓ ↓H␈↓definition␈α
we␈αhave␈α
no␈α
guarantee␈αthat␈α
it␈α
terminates␈αfor␈α
all␈α
arguments.␈α Sometimes␈α
the␈α
problem␈αis␈α
to
␈↓ ↓H␈↓prove␈α∀that␈α∀the␈α∀computation␈α∀terminates,␈α∀sometimes␈α∃the␈α∀problem␈α∀is␈α∀to␈α∀prove␈α∀that␈α∃it␈α∀doesn't,
␈↓ ↓H␈↓sometimes␈α
we␈α
must␈α
establish␈α
that␈α
it␈α
terminates␈α
for␈α
arguments␈α
in␈α
a␈α
certain␈α
set␈α
and␈α
not␈α
otherwise,
␈↓ ↓H␈↓and␈α⊗sometimes␈α∃we␈α⊗want␈α∃to␈α⊗establish␈α∃that␈α⊗two␈α∃function␈α⊗definitions␈α∃are␈α⊗equivalent␈α∃without
␈↓ ↓H␈↓determining for what values either terminates.

␈↓ ↓H␈↓␈↓ α_Even␈αthough␈αa␈αrecursively␈αdefined␈αfunction␈αis␈αnot␈αknown␈αto␈αterminate,␈αit␈αis␈αstill␈αpossible␈αto
␈↓ ↓H␈↓characterize in first order logic.  This is done as follows:

␈↓ ↓H␈↓␈↓ α_Consider␈α∪the␈α∪domain␈α∪␈↓↓SE␈↓␈α∀of␈α∪S-expressions␈α∪to␈α∪be␈α∀imbedded␈α∪in␈α∪a␈α∪larger␈α∀domain.␈α∪ For
␈↓ ↓H␈↓concreteness␈αwe␈α
may␈αsuppose␈αthat␈α
this␈αdomain␈αhas␈α
only␈αone␈αelement␈α
␈↓	w␈↓␈αbesides␈α
the␈αS-expressions
␈↓ ↓H␈↓that␈αwe␈αwill␈αtake␈αas␈αthe␈αvalue␈αof␈αa␈αfunction␈αwhenever␈αits␈αcomputation␈αfails␈αto␈αterminate.␈α We␈αmay
␈↓ ↓H␈↓further␈αassume␈αthat␈αthe␈αbasic␈αLisp␈αfunctions␈αtake␈α␈↓	w␈↓␈αas␈αvalue␈αwhenever␈αan␈αargument␈αhas␈αvalue␈α␈↓	w␈↓.
␈↓ ↓H␈↓However,␈αneither␈αassumption␈αwill␈αever␈αbe␈αused␈αin␈αa␈αproof,␈αso␈αtheir␈αneed␈αbe␈αno␈αaxioms␈αexpressing
␈↓ ↓H␈↓them.

␈↓ ↓H␈↓␈↓ α_Recursive␈αdefinitions␈α
give␈αrise␈α
to␈αlogical␈α
sentences␈αjust␈α
as␈αbefore␈α
so␈αthat␈α
␈↓↓append␈↓␈αis␈α
described
␈↓ ↓H␈↓by
␈↓ ↓H␈↓␈↓ ¬oCHAPTER I␈↓ 99


␈↓ ↓H␈↓5)␈↓ α8  ␈↓↓∀u v.[u * v = ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αa␈↓↓ u . [␈↓αd␈↓↓ u * v]]␈↓,

␈↓ ↓H␈↓but␈α∞now␈α∞it␈α∞is␈α∞not␈α
assumed␈α∞that␈α∞␈↓↓u * v␈↓␈α∞is␈α∞a␈α
list;␈α∞it␈α∞might␈α∞be␈α∞␈↓	w␈↓␈α
or␈α∞any␈α∞other␈α∞element␈α∞of␈α∞the␈α
␈↓↓outer
␈↓ ↓H␈↓↓domain␈↓.  However, we can prove that ␈↓↓u * v␈↓ is a list for all lists ␈↓↓u␈↓ and ␈↓↓v␈↓ by induction as follows:

␈↓ ↓H␈↓␈↓ α_We take

␈↓ ↓H␈↓6)␈↓ α8  ␈↓↓P(u) = islist[u * v]␈↓

␈↓ ↓H␈↓in the axioms schema of list induction getting

␈↓ ↓H␈↓7)␈↓ α8  ␈↓↓islist[␈↓NIL␈↓↓ * v] ∧ ∀u.[¬␈↓αn␈↓↓ u ∧ islist[␈↓αd␈↓↓ u * v] ⊃ islist[u * v]]⊃ ∀u.islist[u * v]␈↓.

␈↓ ↓H␈↓Now␈αthe␈αpremisses␈αof␈α(7)␈αare␈αeasily␈αproved␈αfrom␈α(5)␈αand␈α
the␈αfact␈αthat␈αif␈α␈↓↓u␈↓␈αis␈αa␈αlist,␈αso␈αis␈α␈↓↓x . u␈↓.␈α
 As
␈↓ ↓H␈↓we␈α⊂shall␈α⊂see,␈α⊂the␈α⊂resulting␈α⊂proof␈α⊂that␈α⊂the␈α⊂computation␈α⊂of␈α⊂␈↓↓u * v␈↓␈α⊂is␈α⊂a␈α⊂list␈α⊂can␈α⊂be␈α⊂taken␈α⊂as␈α∂also
␈↓ ↓H␈↓proving that the computation terminates.